The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2))
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2))
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1))
circ(circ(z0, z1), z2) → circ(z0, circ(z1, z2))
circ(z0, id) → z0
circ(id, z0) → z0
circ(cons(lift, z0), circ(cons(lift, z1), z2)) → circ(cons(lift, circ(z0, z1)), z2)
subst(z0, id) → z0
msubst(z0, id) → z0
msubst(msubst(z0, z1), z2) → msubst(z0, circ(z1, z2))

Tuples:

CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1))
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2))
CIRC(cons(lift, z0), circ(cons(lift, z1), z2)) → c6(CIRC(cons(lift, circ(z0, z1)), z2), CIRC(z0, z1))
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))

S tuples:

CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1))
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2))
CIRC(cons(lift, z0), circ(cons(lift, z1), z2)) → c6(CIRC(cons(lift, circ(z0, z1)), z2), CIRC(z0, z1))
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))

K tuples:none
Defined Rule Symbols:

circ, subst, msubst

Defined Pair Symbols:

CIRC, MSUBST

Compound Symbols:

c, c1, c2, c3, c6, c9

(3) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

CIRC(cons(lift, z0), circ(cons(lift, z1), z2)) → c6(CIRC(cons(lift, circ(z0, z1)), z2), CIRC(z0, z1))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2))
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2))
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1))
circ(circ(z0, z1), z2) → circ(z0, circ(z1, z2))
circ(z0, id) → z0
circ(id, z0) → z0
circ(cons(lift, z0), circ(cons(lift, z1), z2)) → circ(cons(lift, circ(z0, z1)), z2)
subst(z0, id) → z0
msubst(z0, id) → z0
msubst(msubst(z0, z1), z2) → msubst(z0, circ(z1, z2))

Tuples:

CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1))
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2))
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))

S tuples:

CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1))
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2))
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))

K tuples:none
Defined Rule Symbols:

circ, subst, msubst

Defined Pair Symbols:

CIRC, MSUBST

Compound Symbols:

c, c1, c2, c3, c9

(5) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2))

We considered the (Usable) Rules:

circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2))
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2))
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1))
circ(circ(z0, z1), z2) → circ(z0, circ(z1, z2))
circ(z0, id) → z0
circ(id, z0) → z0
msubst(z0, id) → z0
msubst(msubst(z0, z1), z2) → msubst(z0, circ(z1, z2))

And the Tuples:

CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1))
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2))
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CIRC(x₁, x₂)) = [4]x₁   
POL(MSUBST(x₁, x₂)) = [2]x₁   
POL(c(x₁, x₂)) = x₁ + x₂   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c9(x₁, x₂)) = x₁ + x₂   
POL(circ(x₁, x₂)) = [1] + [2]x₁ + [3]x₂   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(id) = 0   
POL(lift) = 0   
POL(msubst(x₁, x₂)) = [4] + [2]x₁ + [2]x₂   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2))
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2))
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1))
circ(circ(z0, z1), z2) → circ(z0, circ(z1, z2))
circ(z0, id) → z0
circ(id, z0) → z0
circ(cons(lift, z0), circ(cons(lift, z1), z2)) → circ(cons(lift, circ(z0, z1)), z2)
subst(z0, id) → z0
msubst(z0, id) → z0
msubst(msubst(z0, z1), z2) → msubst(z0, circ(z1, z2))

Tuples:

CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1))
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2))
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))

S tuples:

CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1))
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))

K tuples:

CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2))

Defined Rule Symbols:

circ, subst, msubst

Defined Pair Symbols:

CIRC, MSUBST

Compound Symbols:

c, c1, c2, c3, c9

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))

We considered the (Usable) Rules:

circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2))
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2))
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1))
circ(circ(z0, z1), z2) → circ(z0, circ(z1, z2))
circ(z0, id) → z0
circ(id, z0) → z0
msubst(z0, id) → z0
msubst(msubst(z0, z1), z2) → msubst(z0, circ(z1, z2))

And the Tuples:

CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1))
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2))
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CIRC(x₁, x₂)) = [2] + [2]x₁   
POL(MSUBST(x₁, x₂)) = x₁   
POL(c(x₁, x₂)) = x₁ + x₂   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c9(x₁, x₂)) = x₁ + x₂   
POL(circ(x₁, x₂)) = [1] + [2]x₁ + x₂   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(id) = 0   
POL(lift) = 0   
POL(msubst(x₁, x₂)) = [4] + [4]x₁ + [5]x₂   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2))
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2))
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1))
circ(circ(z0, z1), z2) → circ(z0, circ(z1, z2))
circ(z0, id) → z0
circ(id, z0) → z0
circ(cons(lift, z0), circ(cons(lift, z1), z2)) → circ(cons(lift, circ(z0, z1)), z2)
subst(z0, id) → z0
msubst(z0, id) → z0
msubst(msubst(z0, z1), z2) → msubst(z0, circ(z1, z2))

Tuples:

CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1))
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2))
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))

S tuples:

CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1))

K tuples:

CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2))
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))

Defined Rule Symbols:

circ, subst, msubst

Defined Pair Symbols:

CIRC, MSUBST

Compound Symbols:

c, c1, c2, c3, c9

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1))

We considered the (Usable) Rules:

circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2))
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2))
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1))
circ(circ(z0, z1), z2) → circ(z0, circ(z1, z2))
circ(z0, id) → z0
circ(id, z0) → z0
msubst(z0, id) → z0
msubst(msubst(z0, z1), z2) → msubst(z0, circ(z1, z2))

And the Tuples:

CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1))
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2))
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CIRC(x₁, x₂)) = [3] + x₁   
POL(MSUBST(x₁, x₂)) = [2] + x₁   
POL(c(x₁, x₂)) = x₁ + x₂   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c9(x₁, x₂)) = x₁ + x₂   
POL(circ(x₁, x₂)) = [4] + x₁ + x₂   
POL(cons(x₁, x₂)) = [5] + x₁ + x₂   
POL(id) = 0   
POL(lift) = 0   
POL(msubst(x₁, x₂)) = [3] + x₁ + x₂   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2))
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2))
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1))
circ(circ(z0, z1), z2) → circ(z0, circ(z1, z2))
circ(z0, id) → z0
circ(id, z0) → z0
circ(cons(lift, z0), circ(cons(lift, z1), z2)) → circ(cons(lift, circ(z0, z1)), z2)
subst(z0, id) → z0
msubst(z0, id) → z0
msubst(msubst(z0, z1), z2) → msubst(z0, circ(z1, z2))

Tuples:

CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1))
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2))
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))

S tuples:

CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2))

K tuples:

CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2))
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1))

Defined Rule Symbols:

circ, subst, msubst

Defined Pair Symbols:

CIRC, MSUBST

Compound Symbols:

c, c1, c2, c3, c9

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2))

We considered the (Usable) Rules:

circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2))
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2))
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1))
circ(circ(z0, z1), z2) → circ(z0, circ(z1, z2))
circ(z0, id) → z0
circ(id, z0) → z0
msubst(z0, id) → z0
msubst(msubst(z0, z1), z2) → msubst(z0, circ(z1, z2))

And the Tuples:

CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1))
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2))
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CIRC(x₁, x₂)) = [2] + [2]x₁   
POL(MSUBST(x₁, x₂)) = [4] + [2]x₁   
POL(c(x₁, x₂)) = x₁ + x₂   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c9(x₁, x₂)) = x₁ + x₂   
POL(circ(x₁, x₂)) = [3] + [4]x₁ + x₂   
POL(cons(x₁, x₂)) = [3] + x₁ + x₂   
POL(id) = 0   
POL(lift) = 0   
POL(msubst(x₁, x₂)) = [4] + [4]x₁ + x₂   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

circ(cons(z0, z1), z2) → cons(msubst(z0, z2), circ(z1, z2))
circ(cons(lift, z0), cons(z1, z2)) → cons(z1, circ(z0, z2))
circ(cons(lift, z0), cons(lift, z1)) → cons(lift, circ(z0, z1))
circ(circ(z0, z1), z2) → circ(z0, circ(z1, z2))
circ(z0, id) → z0
circ(id, z0) → z0
circ(cons(lift, z0), circ(cons(lift, z1), z2)) → circ(cons(lift, circ(z0, z1)), z2)
subst(z0, id) → z0
msubst(z0, id) → z0
msubst(msubst(z0, z1), z2) → msubst(z0, circ(z1, z2))

Tuples:

CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1))
CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2))
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))

S tuples:none
K tuples:

CIRC(circ(z0, z1), z2) → c3(CIRC(z0, circ(z1, z2)), CIRC(z1, z2))
MSUBST(msubst(z0, z1), z2) → c9(MSUBST(z0, circ(z1, z2)), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(lift, z1)) → c2(CIRC(z0, z1))
CIRC(cons(z0, z1), z2) → c(MSUBST(z0, z2), CIRC(z1, z2))
CIRC(cons(lift, z0), cons(z1, z2)) → c1(CIRC(z0, z2))

Defined Rule Symbols:

circ, subst, msubst

Defined Pair Symbols:

CIRC, MSUBST

Compound Symbols:

c, c1, c2, c3, c9

(13) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(14) BOUNDS(O(1), O(1))